package arlab.formulae

/**
 * Created by IntelliJ IDEA.
 * User: Eve
 * Date: 23.02.12
 * Time: 12:18
 * To change this template use File | Settings | File Templates.
 */

// And, Or, Not sind Funktionen von Formeln
trait Formula{

  def &&(that: Formula) = And(this, that)
  def ||(that: Formula) = Or(this,that)
  def unary_- = Not(this)

  def transform(f: Formula => Formula) = f(this)
  def free:Set[Variable]=freeHelp(Set():Set[Variable]):Set[Variable]
  def bound:Set[Variable] =Set()
  def freeHelp(bound:Set[Variable]):Set[Variable]=Set()

  def renameAllVariables(i:Int):Formula = this
  
  def functions: Set[(String,Int)] = Set()

  //substituiert alle Variablen aus der uebergebenen map  
  def subst(sfn: Map[Variable, Term]): Formula = this
  
  
  def implic(a:Formula):Formula = And(Or(a, Not(this)), Or(Not(a), this))
  def tseit_implic(a:Formula):Formula = a match {
     case And(a,b) => And(And(Or(Not(this), a), 
                              Or(Not(this), b)), 
                          Or(this, Or(Not(a), Not(b))))
     case Or(a,b) => And(And(Or(Not(this), 
                                Or(a,b)), 
                             Or(this, Not(a))),
                         Or(this, Not(b)))
  
  }  
}


// eine Variable besteht nur aus einem Namen
case class BooleanVariable(name:String) extends Formula {
  override 
  def toString()=    name

  override def renameAllVariables(i:Int):Formula = BooleanVariable(name + i)

  //gibt eine Liste zurück die Alle Funktionen mitsammt ihren Stelligkeiten zurückgibt.
  override def functions: Set[(String,Int)] = Set((name, 0))
}
